T:Type, eq:EqDecider(T), es:ES, x:Id, e:E.
@loc(e)(x:T)  (lastchange(x;e) < e)  ((x after lastchange(x;e)) = (x when e)  T) 

latex

Definitions	loc(e), e[e1,e2).P(e), e@i. P(e), , discrete(i;x), vartype(i;x), lastchange(x;e), (e <loc e'), P  Q, P & Q, P  Q, P  Q, x:AB(x), (e < e'), e < e', @i(x:T), E, t.1, s = t, Id, Atom$n, ES, EqDecider(T), x:A  B(x), Type, isrcv(e), b, x:A. B(x), t  T
Lemmas	es-loc wf, es-isrcv-loc, es-dtype wf, es-loc-lc, es-lc wf, es-le weakening eq, es-vartype wf, es-isconst wf, assert wf, es-causl wf, es-E wf, Id wf, event system wf, deq wf, es-lc-after